A B C D E F G H I J K L M N O P Q R S T U V W X Y Z All
Yadav, Divakar
- Formal Verification of Distributed Checkpointing Using Event-B
Authors
1 Department of Computer Science and Engineering, Institute of Engineering and Technology, Lucknow, Uttar Pradesh 226021, IN
2 Department of Computer Science and Engineering, Pranveer Singh Institute of Technology, Kanpur, Uttar Pradesh 209305, IN
Source
AIRCC's International Journal of Computer Science and Information Technology, Vol 7, No 5 (2015), Pagination: 59-73Abstract
The development of complex system makes challenging task for correct software development. Due to faulty specification, software may involve errors. The traditional testing methods are not sufficient to verify the correctness of such complex system. In order to capture correct system requirements and rigorous reasoning about the problems, formal methods are required. Formal methods are mathematical techniques that provide precise specification of problems with their solutions and proof of correctness. In this paper, we have done formal verification of check pointing process in a distributed database system using Event B. Event-B is an event driven formal method which is used to develop formal models of distributed database systems. In a distributed database system, the database is stored at different sites that are connected together through the network. Checkpoint is a recovery point which contains the state information about the site. In order to do recovery of a distributed transaction a global checkpoint number (GCPN) is required. A global checkpoint number decides which transaction will be included for recovery purpose. All transactions whose timestamp are less than global checkpoint number will be marked as before checkpoint transaction (BCPT) and will be considered for recovery purpose. The transactions whose timestamp are greater than GCPN will be marked as after checkpoint transaction (ACPT) and will be part of next global checkpoint number.Keywords
Formal Methods, Formal Specifications, Formal Verification, Event-B, Distributed Transaction, Checkpointing, Local checkpoint Number, Global Checkpoint Number.- Formal Specification and Verification of Total Order Broadcast through Destination Agreement Using Event-B
Authors
1 Department of Electronics Engg., IET, Lucknow, IN
2 Department of Computer Science and Engg., IET, Lucknow, IN
Source
AIRCC's International Journal of Computer Science and Information Technology, Vol 7, No 5 (2015), Pagination: 85-95Abstract
A reliable broadcast is communication primitive used to develop fault tolerant distributed applications. It in due course delivers messages to all participating sites irrespective of their ordering. Total order broadcast impose restriction on message ordering and satisfies total order requirement.
A clear specifications, rigorous validation and verification is key to obtain better design of dependable services in such applications. With the help of formal methods one can specify and verify systems in systematic rather than ad hoc manner. It reveals ambiguities, incompleteness, and inconsistencies in a system by facilitating clear specification, rigorous validation and verification.
In this paper, we present a formal development of total order broadcast. The model have been developed and checked by using event-B techniques supported by the RODIN tool. Event-B is a formal technique that supports the incremental design of a distributed applications using notion of refinements.
Keywords
Total Order Broadcast, Event-B, Reliable Broadcast.- A Novel Technique for Back-Link Extraction and Relevance Evaluation
Authors
1 Department of Computer Science Engineering, MAIT, Rohini, New Delhi, IN
2 Department of Computer, YMCA University of Science and Technology, Faridabad, IN
3 Department of Computer Science and Information, JIITU, Noida, IN